A:Type, l:A List. ||l||1 

latex

Definitions	t  T, x:A. B(x), ||as||, i<j, b, P  Q, False, A, AB, ij, A List, P & Q, P  Q, True, T, SqStable(P)
Lemmas	sq stable from decidable, decidable le, le wf, assert of lt int, assert wf, lt int wf, length wf1